(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (not (exists ((q0 (_ BitVec 10))) (not (= (_ bv591 10) (_ bv591 10) q0 q0)))))
(assert (not (forall ((q1 (_ BitVec 1)) (q2 (_ BitVec 1)) (q3 (_ BitVec 1)) (q4 (_ BitVec 1))) (not (= (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)))))))
(declare-const v17 Bool)
(assert (not (exists ((q5 (_ BitVec 1)) (q6 Bool) (q7 Bool)) (=> (= v0 q7 v1 q6 v17 q6 q7 v12 q6) (distinct (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)))))))
(assert (or (forall ((q5 (_ BitVec 1)) (q6 Bool) (q7 Bool)) (=> (or q7 v4 v6) (= q5 (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) q5 (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))))) (exists ((q5 (_ BitVec 1)) (q6 Bool) (q7 Bool)) (=> (and q7 q6 q7 (xor v10 v5 v15 v13 (xor v1 v3 v5 v4) (distinct (_ bv591 10) (_ bv591 10) (_ bv591 10)) v12 v10 (and v6 v10)) q7 q6 (and v16 v16 v12 (and v6 v10))) (= (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) q5)))))
(assert (not (exists ((q8 Bool)) (not (and (distinct (_ bv591 10) (_ bv591 10) (_ bv591 10) (_ bv591 10)) q8)))))
(declare-const v18 Bool)
(assert (not (forall ((q9 (_ BitVec 1)) (q10 (_ BitVec 10)) (q11 Bool)) (xor (distinct (bvsmod (_ bv591 10) (_ bv591 10)) q10 (bvsmod (_ bv591 10) (_ bv591 10))) (and (= (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) v16 q11 (distinct (_ bv591 10) (_ bv591 10) (_ bv591 10) (_ bv591 10)) q11 q11 q11 q11 q11) (= (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) q9)))))
(assert (exists ((q12 (_ BitVec 10))) v5))
(assert (not (exists ((q13 (_ BitVec 1)) (q14 Bool)) (=> (distinct v5 q14 q14 q14 q14 v0) (= (bvudiv (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)))) (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) q13 q13)))))
(assert (or (forall ((q13 (_ BitVec 1)) (q14 Bool)) v9) (exists ((q13 (_ BitVec 1)) (q14 Bool)) (=> (=> (= (and v6 v10) v3 v16) v0) (distinct (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvudiv (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)))) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) q13)))))
(declare-const v19 Bool)
(assert (exists ((q15 (_ BitVec 12)) (q16 (_ BitVec 10)) (q17 (_ BitVec 10)) (q18 (_ BitVec 1))) (= (bvslt q17 q16) (bvsle q15 #x1bc) (= (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) q18 q18 q18))))
(assert (exists ((q19 (_ BitVec 1)) (q20 Bool) (q21 (_ BitVec 11)) (q22 (_ BitVec 1))) (=> (bvslt (concat (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvsrem (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) q21) (=> v0 q20))))
(declare-const _5-0 (_ BitVec 5))
(assert (forall ((q23 (_ BitVec 10)) (q24 (_ BitVec 12)) (q25 (_ BitVec 12)) (q26 (_ BitVec 1))) (= (bvuge q24 #x1bc) (distinct q23 q23 q23 (bvsmod (_ bv591 10) (_ bv591 10))) (= (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvudiv (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10))) (bvnor (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)) (bvcomp (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv534 10)))) q26))))
(assert (not (forall ((q27 (_ BitVec 11)) (q28 (_ BitVec 11))) (distinct #x328 #x328 #x328))))
(assert (or v9))
(assert (or v9 v0 v10 v10))
(assert (or v10 (distinct (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv591 10) (_ bv591 10) (_ bv534 10) (_ bv591 10)) (distinct (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv591 10) (_ bv591 10) (_ bv534 10) (_ bv591 10))))
(assert (or v9 (distinct (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv591 10) (_ bv591 10) (_ bv534 10) (_ bv591 10)) (distinct #x328 #x328 #x328) v9 v9 (distinct (bvsmod (_ bv591 10) (_ bv591 10)) (_ bv591 10) (_ bv591 10) (_ bv534 10) (_ bv591 10)) v9 v9))
(assert (or v0 v10))
(assert (or v0 v0 v13 (distinct #x328 #x328 #x328) (distinct #x328 #x328 #x328) v9))
(check-sat)
